package algorithms.chromatic;

/**
 * Implementation of dictionary ADT with a non-blocking chromatic search tree.
 * Copyright (C) 2013 Trevor Brown
 * Contact (me [at] tbrown [dot] pro) with questions or comments.
 *
 * Details of the chromatic search tree algorithm appear in the paper:
 *    "A general technique for non-blocking trees"
 * by Trevor Brown (Univeristy of Toronto)
 *    Faith Ellen  (University of Toronto)
 *    Eric Ruppert (York University)
 * 
 * This optimized version performs rebalancing only once a path from the root
 * to a leaf contains at least d violations of the red-black tree invariants,
 * where d is a constant specified when an instance of the tree is created.
 * Increasing d decreases the number of rotations that must be performed
 * at the cost of increasing search time. Since searches are extremely fast,
 * this trade off is often very beneficial for moderate values of d.
 * When d = 0, each put() or remove() fixes any violation it created before
 * returning to the caller.
 *
 * This data structure has:
 *  -- entirely non-blocking (also called lock-free) operations
 *  -- height that is O(c+d+log n), where n is the number of keys in the
 *     dictionary, d is the constant mentioned above, and c is the number of
 *     insertions and deletions currently in progress.
 *     (the constants hidden by the big-O notation are small.)
 * 
 * If there is interest in using this data structure, but it lacks some basic
 * functionality that is required, Trevor Brown is open to expanding this work.
 * For instance, it is possible to add:
 *  -- the ability to atomically { remove any number of nodes/keys/values
 *     (even if they are scattered throughout the tree), and add one },
 *  -- linearizable size(), clone(), iterators, range queries, and
 *  -- the ability to compose operations by layering transactional memory
 *     on top of the fast non-blocking operations offered by this tree.
 * 
 * As an interesting side note, less than 550 lines of code in this file were
 * written by hand.  The remainder were generated by a computer program,
 * which can be adapted to produce code for other balanced trees.
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 */

import java.util.Comparator;
import java.util.concurrent.atomic.AtomicReferenceFieldUpdater;

public class LockFreeChromaticMap<K,V> {
    private final int d; // this is the number of violations to allow on a search path before we fix everything on it. if d is zero, then each update fixes any violation it created before returning.
    private static final int DEFAULT_d = 6; // experimentally determined to yield good performance for both random workloads, and operations on sorted sequences
    private final Node root;
    private final Operation dummy;
    private final Comparator<? super K> comparator;
    private final AtomicReferenceFieldUpdater<LockFreeChromaticMap.Node, LockFreeChromaticMap.Operation> updateOp;
    private final AtomicReferenceFieldUpdater<LockFreeChromaticMap.Node, LockFreeChromaticMap.Node> updateLeft, updateRight;
    
    public LockFreeChromaticMap() {
        this(DEFAULT_d, null); 
    }
    public LockFreeChromaticMap(final Comparator<? super K> cmp) {
        this(DEFAULT_d, cmp);
    }
    public LockFreeChromaticMap(final int allowedViolationsPerPath) {
        this(allowedViolationsPerPath, null);
    }
    public LockFreeChromaticMap(final int allowedViolationsPerPath, final Comparator<? super K> cmp) {
        d = allowedViolationsPerPath;
        comparator = cmp;
        dummy = new Operation();
        root = new Node(null, null, 1, new Node(null, null, 1, null, null, dummy), null, dummy);
        updateOp = AtomicReferenceFieldUpdater.newUpdater(Node.class, Operation.class, "op");
        updateLeft = AtomicReferenceFieldUpdater.newUpdater(Node.class, Node.class, "left");
        updateRight = AtomicReferenceFieldUpdater.newUpdater(Node.class, Node.class, "right");
        
    }

    /**
     * size() is NOT a constant time method, and the result is only guaranteed to
     * be consistent if no concurrent updates occur.
     * Note: linearizable size() and iterators can be implemented, so contact
     *       the author if they are needed for some application.
     */
    public final int size() {
        return sequentialSize(root);
    }
    private int sequentialSize(final Node node) {
        if (node == null) return 0;
        if (node.left == null && node.key != null) return 1;
        return sequentialSize(node.left) + sequentialSize(node.right);
    }

    public final boolean containsKey(final K key) {
        return get(key) != null;
    }

    public final V get(final K key) {
        final Comparable<? super K> k = comparable(key);
        Node l = root.left.left;
        if (l == null) return null; // no keys in data structure
        while (l.left != null) {
            l = (k.compareTo((K) l.key) < 0) ? l.left : l.right;
        }
        return (k.compareTo((K) l.key) == 0) ? (V) l.value : null;
    }

    public final V put(final K key, final V value) {
        return doPut(key, value, false);
    }

    public final V putIfAbsent(final K key, final V value) {
        return doPut(key, value, true);
    }

    private V doPut(final K key, final V value, final boolean onlyIfAbsent) {
        final Comparable<? super K> k = comparable(key);
        boolean found = false;
        Operation op = null;
        Node p = null, l = null;
        int count = 0;
        
        while (true) {
            while (op == null) {
                p = root;
                l = root.left;
                if (l.left != null) {
                    count = 0;
                    p = l;
                    l = l.left; // note: before executing this line, l must have key infinity, and l.left must not.
                    while (l.left != null) {
                        if (d > 0 && (l.weight > 1 || l.weight == 0 && p.weight == 0)) ++count;
                        p = l;
                        l = (k.compareTo((K) l.key) < 0) ? l.left : l.right;
                    }
                }
                
                // if we find the key in the tree already
                if (l.key != null && k.compareTo((K) l.key) == 0) {
                    found = true;
                    if (onlyIfAbsent) return (V) l.value;
                    op = createReplaceOp(p, l, key, value);
                } else {
                    found = false;
                    op = createInsertOp(p, l, key, value, k);
                }
            }
            if (helpSCX(op, 0)) {
                // clean up violations if necessary
                if (d == 0) {
                    if (!found && p.weight == 0 && l.weight == 1) fixToKey(k);
                } else {
                    if (count >= d) fixToKey(k);
                }
                // we may have found the key and replaced its value (and, if so, the old value is stored in the old node)
                return (found ? (V) l.value : null);
            }
            op = null;
        }
    }

    public final V remove(final K key) {
        final Comparable<? super K> k = comparable(key);
        Node gp, p = null, l = null;
        Operation op = null;
        int count = 0;
        
        while (true) {
            while (op == null) {
                gp = root;
                p = root;
                l = root.left;
                if (l.left != null) {
                    count = 0;
                    gp = p;
                    p = l;
                    l = l.left; // note: before executing this line, l must have key infinity, and l.left must not.
                    while (l.left != null) {
                        if (d > 0 && (l.weight > 1 || l.weight == 0 && p.weight == 0)) ++count;
                        gp = p;
                        p = l;
                        l = (k.compareTo((K) l.key) < 0) ? l.left : l.right;
                    }
                }
                
                // the key was not in the tree at the linearization point, so no value was removed
                if (l.key == null || k.compareTo((K) l.key) != 0) return null;
                op = createDeleteOp(gp, p, l);
            }
            if (helpSCX(op, 0)) {
                // clean up violations if necessary
                if (d == 0) {
                    if (p.weight > 0 && l.weight > 0 && !isSentinel(p)) fixToKey(k);
                } else {
                    if (count >= d) fixToKey(k);
                }
                // we deleted a key, so we return the removed value (saved in the old node)
                return (V) l.value;
            }
            op = null;
        }
    }

    public final void fixToKey(final Comparable<? super K> k) {
        while (true) {
            Node ggp, gp, p, l = root.left;
            if (l.left == null) return; // only sentinels in tree...
            ggp = gp = root;
            p = l;
            l = l.left; // note: before executing this line, l must have key infinity, and l.left must not.
            while (l.left != null && l.weight <= 1 && (l.weight != 0 || p.weight != 0)) {
                ggp = gp;
                gp = p;
                p = l;
                l = (k.compareTo((K) l.key) < 0) ? l.left : l.right;
            }
            if (l.weight == 1) return; // if no violation, then the search hit a leaf, so we can stop

            final Operation op = createBalancingOp(ggp, gp, p, l);
            if (op != null) {
                helpSCX(op, 0);
            }
        }
    }

    @SuppressWarnings("unchecked")
    private Comparable<? super K> comparable(final Object key) {
        if (key == null) {
            throw new NullPointerException();
        }
        if (comparator == null) {
            return (Comparable<? super K>)key;
        }
        return new Comparable<K>() {
            @SuppressWarnings("unchecked")
            public int compareTo(final K rhs) { return comparator.compare((K)key, rhs); }
        };
    }
    
    private boolean isSentinel(final Node node) {
        return (node.key == null || node == root.left.left);
    }
    
    // This weaker form of LLX does not return a linearizable snapshot.
    // However, we do not use the fact that LLX returns a snapshot anywhere in
    //   the proof of SCX (help), and we do not need the snapshot capability
    //   to satisfy the precondition of SCX (that there be an LLX linked to SCX
    //   for each node in V).
    // Note: using a full LLX slows things by ~3%.
    private Operation weakLLX(final Node r) {
        final Operation rinfo = r.op;
        final int state = rinfo.state;
        if (state == Operation.STATE_ABORTED || (state == Operation.STATE_COMMITTED && !r.marked)) {
            return rinfo;
        }
        if (rinfo.state == Operation.STATE_INPROGRESS) {
            helpSCX(rinfo, 1);
        } else if (r.op.state == Operation.STATE_INPROGRESS) {
            helpSCX(r.op, 1);
        }
        return null;
    }
    // helper function to use the results of a weakLLX more conveniently
    private boolean weakLLX(final Node r, final int i, final Operation[] ops, final Node[] nodes) {
        if ((ops[i] = weakLLX(r)) == null) return false;
        nodes[i] = r;
        return true;
    }
    
    // this function is essentially an SCX without the creation of V, R, fld, new
    // (which are stored in an operation object).
    // the creation of the operation object is simply inlined in other methods.
    private boolean helpSCX(final Operation op, int i) {
        // get local references to some fields of op, in case we later null out fields of op (to help the garbage collector)
        final Node[] nodes = op.nodes;
        final Operation[] ops = op.ops;
        final Node subtree = op.subtree;
        // if we see aborted or committed, no point in helping (already done).
        // further, if committed, variables may have been nulled out to help the garbage collector.
        // so, we return.
        if (op.state != Operation.STATE_INPROGRESS) return true;
        
        // freeze sub-tree
        for (; i<ops.length; ++i) {
            if (!updateOp.compareAndSet(nodes[i], ops[i], op) && nodes[i].op != op) { // if work was not done
                if (op.allFrozen) {
                    return true;
                } else {
                    op.state = Operation.STATE_ABORTED;
                    // help the garbage collector (must be AFTER we set state committed or aborted)
                    op.nodes = null;
                    op.ops = null;
                    op.subtree = null;
                    return false;
                }
            }
        }
        op.allFrozen = true;
        for (i=1; i<ops.length; ++i) nodes[i].marked = true; // finalize all but first node
        
        // CAS in the new sub-tree (child-cas)
        if (nodes[0].left == nodes[1]) {
            updateLeft.compareAndSet(nodes[0], nodes[1], subtree);     // splice in new sub-tree (as a left child)
        } else { // assert: nodes[0].right == nodes[1]
            updateRight.compareAndSet(nodes[0], nodes[1], subtree);    // splice in new sub-tree (as a right child)
        }
        op.state = Operation.STATE_COMMITTED;
        
        // help the garbage collector (must be AFTER we set state committed or aborted)
        op.nodes = null;
        op.ops = null;
        op.subtree = null;
        return true;
    }

    private Operation createInsertOp(final Node p, final Node l, final K key, final V value, Comparable k) {
        final Operation[] ops = new Operation[]{null};
        final Node[] nodes = new Node[]{null, l};

        if (!weakLLX(p, 0, ops, nodes)) return null;

        if (l != p.left && l != p.right) return null;

        // Compute the weight for the new parent node
        final int newWeight = (isSentinel(l) ? 1 : l.weight - 1);               // (maintain sentinel weights at 1)

        // Build new sub-tree
        final Node newLeaf = new Node(key, value, 1, null, null, dummy);
        final Node newL = new Node(l.key, l.value, 1, null, null, dummy);
        final Node newP;
        if (l.key == null || k.compareTo(l.key) < 0) {
            newP = new Node(l.key, l.value, newWeight, newLeaf, newL, dummy);
        } else {
            newP = new Node(key, value, newWeight, newL, newLeaf, dummy);
        }
        return new Operation( nodes, ops, newP);
    }
    
    // Just like insert, except this replaces any existing value.
    private Operation createReplaceOp(final Node p, final Node l, final K key, final V value) {
        final Operation[] ops = new Operation[]{null};
        final Node[] nodes = new Node[]{null, l};

        if (!weakLLX(p, 0, ops, nodes)) return null;

        if (l != p.left && l != p.right) return null;

        // Build new sub-tree
        final Node subtree = new Node(key, value, l.weight, l.left, l.right, dummy);
        return new Operation(nodes, ops, subtree);
    }

    private Operation createDeleteOp(final Node gp, final Node p, final Node l) {
        final Operation[] ops = new Operation[]{null, null, null};
        final Node[] nodes = new Node[]{null, null, null};

        if (!weakLLX(gp, 0, ops, nodes)) return null;
        if (!weakLLX(p, 1, ops, nodes)) return null;
        
        if (p != gp.left && p != gp.right) return null;
        final boolean left = (l == p.left);
        if (!left && l != p.right) return null;

        // Read fields for the sibling of l into ops[2], nodes[2] = s
        if (!weakLLX(left ? p.right : p.left, 2, ops, nodes)) return null;
        final Node s = nodes[2];

        // Now, if the op. succeeds, all structure is guaranteed to be just as we verified

        // Compute weight for the new node (to replace to deleted leaf l and parent p)
        final int newWeight = (isSentinel(p) ? 1 : p.weight + s.weight); // weights of parent + sibling of deleted leaf

        // Build new sub-tree
        final Node newP = new Node(s.key, s.value, newWeight, s.left, s.right, dummy);
        return new Operation(nodes, ops, newP);
    }

    private Operation createBalancingOp(final Node f, final Node fX, final Node fXX, final Node fXXX) {
        final Operation opf = weakLLX(f);
        if (opf == null || !f.hasChild(fX)) return null;

        final Operation opfX = weakLLX(fX);
        if (opfX == null) return null;
        final Node fXL = fX.left;
        final Node fXR = fX.right;
        final boolean fXXleft = (fXX == fXL);
        if (!fXXleft && fXX != fXR) return null;
        
        final Operation opfXX = weakLLX(fXX);
        if (opfXX == null) return null;
        final Node fXXL = fXX.left;
        final Node fXXR = fXX.right;
        final boolean fXXXleft = (fXXX == fXXL);
        if (!fXXXleft && fXXX != fXXR) return null;
        
        // Overweight violation
        if (fXXX.weight > 1) {
            if (fXXXleft) {
                final Operation opfXXL = weakLLX(fXXL);
                if (opfXXL == null) return null;
                return createOverweightLeftOp(f, fX, fXX, fXXL, opf, opfX, opfXX, opfXXL, fXL, fXR, fXXR, fXXleft);

            } else {
                final Operation opfXXR = weakLLX(fXXR);
                if (opfXXR == null) return null;
                return createOverweightRightOp(f, fX, fXX, fXXR, opf, opfX, opfXX, opfXXR, fXR, fXL, fXXL, !fXXleft);
            }
        // Red-red violation
        } else {
            if (fXXleft) {
                if (fXR.weight == 0) {
                    final Operation opfXR = weakLLX(fXR);
                    if (opfXR == null) return null;
                    return createBlkOp(new Node[] {f, fX, fXX, fXR}, new Operation[] {opf, opfX, opfXX, opfXR});
                    
                } else if (fXXXleft) {
                    return createRb1Op(new Node[] {f, fX, fXX}, new Operation[] {opf, opfX, opfXX});
                    
                } else {
                    final Operation opfXXR = weakLLX(fXXR);
                    if (opfXXR == null) return null;
                    return createRb2Op(new Node[] {f, fX, fXX, fXXR}, new Operation[] {opf, opfX, opfXX, opfXXR});
                }
            } else {
                if (fXL.weight == 0) {
                    final Operation opfXL = weakLLX(fXL);
                    if (opfXL == null) return null;
                    return createBlkOp(new Node[] {f, fX, fXL, fXX}, new Operation[] {opf, opfX, opfXL, opfXX});
                    
                } else if (!fXXXleft) {
                    return createRb1SymOp(new Node[] {f, fX, fXX}, new Operation[] {opf, opfX, opfXX});
                    
                } else {
                    final Operation opfXXL = weakLLX(fXXL);
                    if (opfXXL == null) return null;
                    return createRb2SymOp(new Node[] {f, fX, fXX, fXXL}, new Operation[] {opf, opfX, opfXX, opfXXL});
                }
            }
        }
    }
    
    private Operation createOverweightLeftOp(final Node f,
                                             final Node fX,
                                             final Node fXX,
                                             final Node fXXL,
                                             final Operation opf,
                                             final Operation opfX,
                                             final Operation opfXX,
                                             final Operation opfXXL,
                                             final Node fXL,
                                             final Node fXR,
                                             final Node fXXR,
                                             final boolean fXXlef) {
        if (fXXR.weight == 0) {
            if (fXX.weight == 0) {
                if (fXXlef) {
                    if (fXR.weight == 0) {
                        final Operation opfXR = weakLLX(fXR);
                        if (opfXR == null) return null;
                        return createBlkOp(new Node[] {f, fX, fXX, fXR}, new Operation[] {opf, opfX, opfXX, opfXR});
                    } else { // assert: fXR.weight > 0
                        final Operation opfXXR = weakLLX(fXXR);
                        if (opfXXR == null) return null;
                        return createRb2Op(new Node[] {f, fX, fXX, fXXR}, new Operation[] {opf, opfX, opfXX, opfXXR});
                    }
                } else { // assert: fXX == fXR
                    if (fXL.weight == 0) {
                        final Operation opfXL = weakLLX(fXL);
                        if (opfXL == null) return null;
                        return createBlkOp(new Node[] {f, fX, fXL, fXX}, new Operation[] {opf, opfX, opfXL, opfXX});
                    } else {
                        return createRb1SymOp(new Node[] {f, fX, fXX}, new Operation[] {opf, opfX, opfXX});
                    }
                }
            } else { // assert: fXX.weight > 0
                final Operation opfXXR = weakLLX(fXXR);
                if (opfXXR == null) return null;
                
                final Node fXXRL = fXXR.left;
                final Operation opfXXRL = weakLLX(fXXRL);
                if (opfXXRL == null) return null;
                
                if (fXXRL.weight > 1) {
                    return createW1Op(new Node[] {fX, fXX, fXXL, fXXR, fXXRL}, new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXRL});
                } else if (fXXRL.weight == 0) {
                    return createRb2SymOp(new Node[] {fX, fXX, fXXR, fXXRL}, new Operation[] {opfX, opfXX, opfXXR, opfXXRL});
                } else { // assert: fXXRL.weight == 1
                    final Node fXXRLR = fXXRL.right;
                    if (fXXRLR == null) return null;
                    if (fXXRLR.weight == 0) {
                        final Operation opfXXRLR = weakLLX(fXXRLR);
                        if (opfXXRLR == null) return null;
                        return createW4Op(new Node[] {fX, fXX, fXXL, fXXR, fXXRL, fXXRLR}, new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXRL, opfXXRLR});
                    } else { // assert: fXXRLR.weight > 0
                        final Node fXXRLL = fXXRL.left;
                        if (fXXRLL == null) return null;
                        if (fXXRLL.weight == 0) {
                            final Operation opfXXRLL = weakLLX(fXXRLL);
                            if (opfXXRLL == null) return null;
                            return createW3Op(new Node[] {fX, fXX, fXXL, fXXR, fXXRL, fXXRLL}, new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXRL, opfXXRLL});
                        } else { // assert: fXXRLL.weight > 0
                            return createW2Op(new Node[] {fX, fXX, fXXL, fXXR, fXXRL}, new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXRL});
                        }
                    }
                }
            }
        } else if (fXXR.weight == 1) {
            final Operation opfXXR = weakLLX(fXXR);
            if (opfXXR == null) return null;
            
            final Node fXXRL = fXXR.left;
            if (fXXRL == null) return null;
            final Node fXXRR = fXXR.right; // note: if fXXRR is null, then fXXRL is null, since tree is always a full binary tree, and children of leaves don't change
            if (fXXRR.weight == 0) {
                final Operation opfXXRR = weakLLX(fXXRR);
                if (opfXXRR == null) return null;
                return createW5Op(new Node[] {fX, fXX, fXXL, fXXR, fXXRR}, new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXRR});
            } else if (fXXRL.weight == 0) {
                final Operation opfXXRL = weakLLX(fXXRL);
                if (opfXXRL == null) return null;
                return createW6Op(new Node[] {fX, fXX, fXXL, fXXR, fXXRL}, new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXRL});
            } else {
                return createPushOp(new Node[] {fX, fXX, fXXL, fXXR}, new Operation[] {opfX, opfXX, opfXXL, opfXXR});
            }
        } else {
            final Operation opfXXR = weakLLX(fXXR);
            if (opfXXR == null) return null;
            return createW7Op(new Node[] {fX, fXX, fXXL, fXXR}, new Operation[] {opfX, opfXX, opfXXL, opfXXR});
        }
    }
    
    public static final class Node {
        public final int weight;
        public final Object value;
        public volatile boolean marked;
        public volatile Operation op;
        public final Object key;
        public volatile Node left, right;

        public Node(final Object key, final Object value, final int weight, final Node left, final Node right, final Operation op) {
            this.key = key;
            this.value = value;
            this.weight = weight;
            this.left = left;
            this.right = right;
            this.op = op;
        }

        public final boolean hasChild(final Node node) {
            return node == left || node == right;
        }
    }

    public static final class Operation {
        final static int STATE_INPROGRESS = 0;
        final static int STATE_ABORTED = 1;
        final static int STATE_COMMITTED = 2;

        volatile Node subtree;
        volatile Node[] nodes;
        volatile Operation[] ops;
        volatile int state;
        volatile boolean allFrozen;

        public Operation() {            // create an inactive operation (a no-op) [[ we do this to avoid the overhead of inheritance ]]
            nodes = null; ops = null; subtree = null;
            this.state = STATE_ABORTED;   // cheap trick to piggy-back on a pre-existing check for active operations
        }
        
        public Operation(final Node[] nodes, final Operation[] ops, final Node subtree) {
            this.nodes = nodes;
            this.ops = ops;
            this.subtree = subtree;
        }
    }
    
    /**
     *
     * Code for debugging
     *
     */
     
    private int countNodes(final Node node) {
        if (node == null) return 0;
        return 1 + countNodes(node.left) + countNodes(node.right);
    }

    public final int getNumberOfNodes() {
        return countNodes(root);
    }

    private int sumDepths(final Node node, final int depth) {
        if (node == null) return 0;
        return (node.left == null ? depth : 0) + sumDepths(node.left, depth+1) + sumDepths(node.right, depth+1);
    }

    public final int getSumOfDepths() {
        return sumDepths(root, 0);
    }
    
    private long getKeysum(final Node node) {
        if (node == null) return 0;
        if (node.left == null) return (int) (Integer) node.key;
        return getKeysum(node.left) + getKeysum(node.right);
    }
    
    // Returns the sum of keys in the tree (the keys in leaves)
    public final long getKeysum() {
        return getKeysum(root.left.left);
    }
    
    /**
     *
     * Computer generated code
     *
     */
    
    private Operation createOverweightRightOp(final Node f,
                                             final Node fX,
                                             final Node fXX,
                                             final Node fXXR,
                                             final Operation opf,
                                             final Operation opfX,
                                             final Operation opfXX,
                                             final Operation opfXXR,
                                             final Node fXR,
                                             final Node fXL,
                                             final Node fXXL,
                                             final boolean fXXright) {
        if (fXXL.weight == 0) {
            if (fXX.weight == 0) {
                if (fXXright) {
                    if (fXL.weight == 0) {
                        final Operation opfXL = weakLLX(fXL);
                        if (opfXL == null) return null;
                        return createBlkOp(new Node[] {f, fX, fXL, fXX},
                                           new Operation[] {opf, opfX, opfXL, opfXX});
                    } else { // assert: fXL.weight > 0
                        final Operation opfXXL = weakLLX(fXXL);
                        if (opfXXL == null) return null;
                        return createRb2SymOp(new Node[] {f, fX, fXX, fXXL},
                                           new Operation[] {opf, opfX, opfXX, opfXXL});
                    }
                } else { // assert: fXX == fXL
                    if (fXR.weight == 0) {
                        final Operation opfXR = weakLLX(fXR);
                        if (opfXR == null) return null;
                        return createBlkOp(new Node[] {f, fX, fXX, fXR},
                                           new Operation[] {opf, opfX, opfXX, opfXR});
                    } else {
                        return createRb1Op(new Node[] {f, fX, fXX},
                                              new Operation[] {opf, opfX, opfXX});
                    }
                }
            } else { // assert: fXX.weight > 0
                final Operation opfXXL = weakLLX(fXXL);
                if (opfXXL == null) return null;
                
                final Node fXXLR = fXXL.right;
                final Operation opfXXLR = weakLLX(fXXLR);
                if (opfXXLR == null) return null;
                
                if (fXXLR.weight > 1) {
                    return createW1SymOp(new Node[] {fX, fXX, fXXL, fXXR, fXXLR},
                                      new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXLR});
                } else if (fXXLR.weight == 0) {
                    return createRb2Op(new Node[] {fX, fXX, fXXL, fXXLR},
                                          new Operation[] {opfX, opfXX, opfXXL, opfXXLR});
                } else { // assert: fXXLR.weight == 1
                    final Node fXXLRL = fXXLR.left;
                    if (fXXLRL == null) return null;
                    if (fXXLRL.weight == 0) {
                        final Operation opfXXLRL = weakLLX(fXXLRL);
                        if (opfXXLRL == null) return null;
                        return createW4SymOp(new Node[] {fX, fXX, fXXL, fXXR, fXXLR, fXXLRL},
                                          new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXLR, opfXXLRL});
                    } else { // assert: fXXLRL.weight > 0
                        final Node fXXLRR = fXXLR.right;
                        if (fXXLRR == null) return null;
                        if (fXXLRR.weight == 0) {
                            final Operation opfXXLRR = weakLLX(fXXLRR);
                            if (opfXXLRR == null) return null;
                            return createW3SymOp(new Node[] {fX, fXX, fXXL, fXXR, fXXLR, fXXLRR},
                                              new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXLR, opfXXLRR});
                        } else { // assert: fXXLRR.weight > 0
                            return createW2SymOp(new Node[] {fX, fXX, fXXL, fXXR, fXXLR},
                                              new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXLR});
                        }
                    }
                }
            }
        } else if (fXXL.weight == 1) {
            final Operation opfXXL = weakLLX(fXXL);
            if (opfXXL == null) return null;
            
            final Node fXXLR = fXXL.right;
            if (fXXLR == null) return null;
            final Node fXXLL = fXXL.left; // note: if fXXLL is null, then fXXLR is null, since tree is always a full binary tree, and children of leaves don't change
            if (fXXLL.weight == 0) {
                final Operation opfXXLL = weakLLX(fXXLL);
                if (opfXXLL == null) return null;
                return createW5SymOp(new Node[] {fX, fXX, fXXL, fXXR, fXXLL},
                                  new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXLL});
            } else if (fXXLR.weight == 0) {
                final Operation opfXXLR = weakLLX(fXXLR);
                if (opfXXLR == null) return null;
                return createW6SymOp(new Node[] {fX, fXX, fXXL, fXXR, fXXLR},
                                  new Operation[] {opfX, opfXX, opfXXL, opfXXR, opfXXLR});
            } else {
                return createPushSymOp(new Node[] {fX, fXX, fXXL, fXXR},
                                    new Operation[] {opfX, opfXX, opfXXL, opfXXR});
            }
        } else {
            final Operation opfXXL = weakLLX(fXXL);
            if (opfXXL == null) return null;
            return createW7SymOp(new Node[] {fX, fXX, fXXL, fXXR},
                              new Operation[] {opfX, opfXX, opfXXL, opfXXR});
        }
    }
    
    private Operation createBlkOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXL = new Node(nodes[2].key, nodes[2].value, 1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXR = new Node(nodes[3].key, nodes[3].value, 1, nodes[3].left, nodes[3].right, dummy);
        final int weight = (isSentinel(nodes[1]) ? 1 : nodes[1].weight-1); // root of old subtree is a sentinel
        final Node nodeX = new Node(nodes[1].key, nodes[1].value, weight, nodeXL, nodeXR, dummy);
        return new Operation(nodes, ops, nodeX);
    }
    
    private Operation createRb1Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXR = new Node(nodes[1].key, nodes[1].value, 0, nodes[2].right, nodes[1].right, dummy);
        final int weight = nodes[1].weight;
        final Node nodeX = new Node(nodes[2].key, nodes[2].value, weight, nodes[2].left, nodeXR, dummy);
        return new Operation(nodes, ops, nodeX);
    }
    
    private Operation createRb2Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXL = new Node(nodes[2].key, nodes[2].value, 0, nodes[2].left, nodes[3].left, dummy);
        final Node nodeXR = new Node(nodes[1].key, nodes[1].value, 0, nodes[3].right, nodes[1].right, dummy);
        final int weight = nodes[1].weight;
        final Node nodeX = new Node(nodes[3].key, nodes[3].value, weight, nodeXL, nodeXR, dummy);
        return new Operation(nodes, ops, nodeX);
    }
    
    private Operation createPushOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXR = new Node(nodes[3].key, nodes[3].value, 0, nodes[3].left, nodes[3].right, dummy);
        final int weight = (isSentinel(nodes[1]) ? 1 : nodes[1].weight+1); // root of old subtree is a sentinel
        final Node nodeXX = new Node(nodes[1].key, nodes[1].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW1Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXLL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXLR = new Node(nodes[4].key, nodes[4].value, nodes[4].weight-1, nodes[4].left, nodes[4].right, dummy);
        final Node nodeXXL = new Node(nodes[1].key, nodes[1].value, 1, nodeXXLL, nodeXXLR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[3].key, nodes[3].value, weight, nodeXXL, nodes[3].right, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW2Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXLL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXLR = new Node(nodes[4].key, nodes[4].value, 0, nodes[4].left, nodes[4].right, dummy);
        final Node nodeXXL = new Node(nodes[1].key, nodes[1].value, 1, nodeXXLL, nodeXXLR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[3].key, nodes[3].value, weight, nodeXXL, nodes[3].right, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW3Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXLLL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXLL = new Node(nodes[1].key, nodes[1].value, 1, nodeXXLLL, nodes[5].left, dummy);
        final Node nodeXXLR = new Node(nodes[4].key, nodes[4].value, 1, nodes[5].right, nodes[4].right, dummy);
        final Node nodeXXL = new Node(nodes[5].key, nodes[5].value, 0, nodeXXLL, nodeXXLR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[3].key, nodes[3].value, weight, nodeXXL, nodes[3].right, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW4Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXLL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXL = new Node(nodes[1].key, nodes[1].value, 1, nodeXXLL, nodes[4].left, dummy);
        final Node nodeXXRL = new Node(nodes[5].key, nodes[5].value, 1, nodes[5].left, nodes[5].right, dummy);
        final Node nodeXXR = new Node(nodes[3].key, nodes[3].value, 0, nodeXXRL, nodes[3].right, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[4].key, nodes[4].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW5Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXLL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXL = new Node(nodes[1].key, nodes[1].value, 1, nodeXXLL, nodes[3].left, dummy);
        final Node nodeXXR = new Node(nodes[4].key, nodes[4].value, 1, nodes[4].left, nodes[4].right, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[3].key, nodes[3].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW6Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXLL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXL = new Node(nodes[1].key, nodes[1].value, 1, nodeXXLL, nodes[4].left, dummy);
        final Node nodeXXR = new Node(nodes[3].key, nodes[3].value, 1, nodes[4].right, nodes[3].right, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[4].key, nodes[4].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW7Op(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final int weight = (isSentinel(nodes[1]) ? 1 : nodes[1].weight+1); // root of old subtree is a sentinel
        final Node nodeXX = new Node(nodes[1].key, nodes[1].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createRb1SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXL = new Node(nodes[1].key, nodes[1].value, 0, nodes[1].left, nodes[2].left, dummy);
        final int weight = nodes[1].weight;
        final Node nodeX = new Node(nodes[2].key, nodes[2].value, weight, nodeXL, nodes[2].right, dummy);
        return new Operation(nodes, ops, nodeX);
    }
    
    private Operation createRb2SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXL = new Node(nodes[1].key, nodes[1].value, 0, nodes[1].left, nodes[3].left, dummy);
        final Node nodeXR = new Node(nodes[2].key, nodes[2].value, 0, nodes[3].right, nodes[2].right, dummy);
        final int weight = nodes[1].weight;
        final Node nodeX = new Node(nodes[3].key, nodes[3].value, weight, nodeXL, nodeXR, dummy);
        return new Operation(nodes, ops, nodeX);
    }
    
    private Operation createPushSymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXL = new Node(nodes[2].key, nodes[2].value, 0, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final int weight = (isSentinel(nodes[1]) ? 1 : nodes[1].weight+1); // root of old subtree is a sentinel
        final Node nodeXX = new Node(nodes[1].key, nodes[1].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW1SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXRL = new Node(nodes[4].key, nodes[4].value, nodes[4].weight-1, nodes[4].left, nodes[4].right, dummy);
        final Node nodeXXRR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final Node nodeXXR = new Node(nodes[1].key, nodes[1].value, 1, nodeXXRL, nodeXXRR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[2].key, nodes[2].value, weight, nodes[2].left, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW2SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXRL = new Node(nodes[4].key, nodes[4].value, 0, nodes[4].left, nodes[4].right, dummy);
        final Node nodeXXRR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final Node nodeXXR = new Node(nodes[1].key, nodes[1].value, 1, nodeXXRL, nodeXXRR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[2].key, nodes[2].value, weight, nodes[2].left, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW3SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXRL = new Node(nodes[4].key, nodes[4].value, 1, nodes[4].left, nodes[5].left, dummy);
        final Node nodeXXRRR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final Node nodeXXRR = new Node(nodes[1].key, nodes[1].value, 1, nodes[5].right, nodeXXRRR, dummy);
        final Node nodeXXR = new Node(nodes[5].key, nodes[5].value, 0, nodeXXRL, nodeXXRR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[2].key, nodes[2].value, weight, nodes[2].left, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW4SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXLR = new Node(nodes[5].key, nodes[5].value, 1, nodes[5].left, nodes[5].right, dummy);
        final Node nodeXXL = new Node(nodes[2].key, nodes[2].value, 0, nodes[2].left, nodeXXLR, dummy);
        final Node nodeXXRR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final Node nodeXXR = new Node(nodes[1].key, nodes[1].value, 1, nodes[4].right, nodeXXRR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[4].key, nodes[4].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW5SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXL = new Node(nodes[4].key, nodes[4].value, 1, nodes[4].left, nodes[4].right, dummy);
        final Node nodeXXRR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final Node nodeXXR = new Node(nodes[1].key, nodes[1].value, 1, nodes[2].right, nodeXXRR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[2].key, nodes[2].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }
    
    private Operation createW6SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXL = new Node(nodes[2].key, nodes[2].value, 1, nodes[2].left, nodes[4].left, dummy);
        final Node nodeXXRR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final Node nodeXXR = new Node(nodes[1].key, nodes[1].value, 1, nodes[4].right, nodeXXRR, dummy);
        final int weight = nodes[1].weight;
        final Node nodeXX = new Node(nodes[4].key, nodes[4].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }

    private Operation createW7SymOp(final Node[] nodes, final Operation[] ops) {
        final Node nodeXXL = new Node(nodes[2].key, nodes[2].value, nodes[2].weight-1, nodes[2].left, nodes[2].right, dummy);
        final Node nodeXXR = new Node(nodes[3].key, nodes[3].value, nodes[3].weight-1, nodes[3].left, nodes[3].right, dummy);
        final int weight = (isSentinel(nodes[1]) ? 1 : nodes[1].weight+1); // root of old subtree is a sentinel
        final Node nodeXX = new Node(nodes[1].key, nodes[1].value, weight, nodeXXL, nodeXXR, dummy);
        return new Operation(nodes, ops, nodeXX);
    }

}